(declare-fun v0 () Bool)
(declare-fun v1 () Bool)
(declare-fun v2 () Bool)
(declare-fun v3 () Bool)
(declare-fun v4 () Bool)
(declare-fun v5 () Bool)
(declare-fun v6 () Bool)
(declare-fun v7 () Bool)
(declare-fun v8 () Bool)
(declare-fun v9 () Bool)
(declare-fun v10 () Bool)
(declare-fun r0 () Real)
(declare-fun r1 () Real)
(declare-fun r3 () Real)
(declare-fun r5 () Real)
(declare-fun r7 () Real)
(declare-fun r8 () Real)
(declare-fun r9 () Real)
(declare-fun r10 () Real)
(declare-fun r11 () Real)
(declare-fun v11 () Bool)
(assert v2)
(declare-fun r13 () Real)
(push)
(declare-fun r14 () Real)
(assert v7)
(assert (forall ((q19 Real) (q20 Real) (q21 Bool) (q22 Bool) (q23 Bool) (q24 Bool) (q25 Real)) (xor (=> (distinct q19 r13) (=> q22 (= r3 r5 r9 r5 r3 r7))) (forall ((q19 Real) (q20 Real) (q21 Bool) (q22 Bool) (q23 Bool) (q24 Bool) (q25 Real)) (not (<= 5614.0 q25 q19))) (forall ((q9 Bool) (q10 Bool) (q11 Real) (q12 Real) (q13 Real) (q14 Bool)) (xor (=> (distinct q14 q10 v11 (= v7 v4) v8 v2 v4 q14) (< q12 5614.0)) (exists ((q9 Bool) (q10 Bool) (q11 Real) (q12 Real) (q13 Real) (q14 Bool)) (not (= r1 5614.0 r1))) v10 (xor v10 v8 v9) (= v7 v4) v7 v2)) (forall ((q9 Bool) (q10 Bool) (q11 Real) (q12 Real) (q13 Real) (q14 Bool)) (xor (=> (distinct q14 q10 v11 (= v7 v4) v8 v2 v4 q14) (< q12 5614.0)) (exists ((q9 Bool) (q10 Bool) (q11 Real) (q12 Real) (q13 Real) (q14 Bool)) (not (= r1 5614.0 r1))) v10 (xor v10 v8 v9) (= v7 v4) v7 v2)) (= r3 r5 r9 r5 r3 r7) v11 v0)))
(check-sat)
